\begin{tabbing}
$\forall$$i$:Id, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, ${\it snd}_{1}$, ${\it snd}_{2}$:${\it kl}$::Knd $\times$ IdLnk fp$\rightarrow$ (:Id $\times$ Top) List.
\\[0ex]${\it snd}_{1}$ $\parallel$ ${\it snd}_{2}$
\\[0ex]$\Rightarrow$ \=(msg{-}spec{-}loc{-}decl(${\it snd}_{1}$ $\oplus$ ${\it snd}_{2}$;$i$;${\it da}$)\+
\\[0ex]$\Leftarrow\!\Rightarrow$ (msg{-}spec{-}loc{-}decl(${\it snd}_{1}$;$i$;${\it da}$) \& msg{-}spec{-}loc{-}decl(${\it snd}_{2}$;$i$;${\it da}$)))
\-
\end{tabbing}